Nuprl Lemma : es-dt-ap
0,22
postcript
pdf
da
,
l
,
tg
:Top. dt(
l
;
da
)(
tg
) ~
da
(rcv(
l
,
tg
))
latex
Definitions
Top
,
t
T
,
x
:
A
.
B
(
x
)
,
compose-fpf(
a
;
b
;
f
)
,
f
(
x
)
,
dt(
l
;
da
)
Lemmas
top
wf
origin
da, l, tg:Top. dt(l;da)(tg) ~ da(rcv(l,tg)) da, l, tg:Top. dt(l;da)(tg) ~ da(rcv(l,tg)) 
Tx:A. B(x)